A, B, C:MsgA. (A ||+ B)  (A ||+ C)  (B ||+ C)  (A  B ||+ C) 

latex

Definitions	t  T, P  Q, x:A. B(x), A ||+ B, M1  M2, P & Q, M1 || M2, M1 ||decl M2, MsgA
Lemmas	ma-compat wf, msga wf, ma-join wf, ma-compat-join, ma-compat-symmetry